////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2008, 2009, 2011 The Mist project                            //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// A Bison file describing the Mist grammar, generating the AST.
/// The generated parser source-code should only be used by the parse.hpp
/// file, which encapsulates the functionality.
///

////////////////////////////////////////////////////////////////////////////////
// Initial Code                                                               //
////////////////////////////////////////////////////////////////////////////////

%code requires {
	#include <string>
	using std::string;
	
	#include <vector>
	using std::vector;
	
	#include <set>
	using std::set;
	
	#include <typeinfo>
	
	#include <boost/foreach.hpp>
	#define foreach BOOST_FOREACH
	
	#include "common/ptr.hpp"
	#include "common/bigint.hpp"
	#include "messages.hpp"
	#include "tree.hpp"
	#include "visitor.hpp"
	
	typedef void* yyscan_t;
	
	typedef Expression TreeExpression;
	
	namespace Detail {
		// Make sure to use TreeExpression when you want the AST node type Expression.
		
		enum ChainType {
			NO_CHAIN,
			IMPLIES_CHAIN,
			COMPARISON_CHAIN
		};
		
		struct Expression {
			Expression(sptr<TreeExpression> e, ChainType c = NO_CHAIN) : expr(e), chain(c) {}
			sptr<TreeExpression> expr;
			ChainType chain;
		};
		
		struct FunctionSignature {
			sptr<FunctionType>        type;
			sptr<Identifier>          name;
			vector<sptr<Identifier> > parameterNames;
			vector<sptr<Identifier> > templateTypeNames;
		};
		
		struct FunctionSections {
			set<sptr<VariableDeclaration> > logicalVars;
			set<sptr<AssertionArea> >       pre;
			set<sptr<AssertionArea> >       post;
			set<sptr<TreeExpression> >      bound;
			set<string>                     KeY;
			set<sptr<CompoundStatement> >   body;
		};
	}
}

////////////////////////////////////////////////////////////////////////////////
// Options                                                                    //
////////////////////////////////////////////////////////////////////////////////

%require "2.3"
%skeleton "glr.cc"
%glr-parser
%defines
%parse-param { sptr<Node>& output }
%parse-param { yyscan_t yyscanner }
%parse-param { wptr<Messages> messages }
%parse-param { string filename }
%parse-param { vector<sptr<Expression> > insertions }
%lex-param { yyscanner }
%locations
%define "parser_class_name" "Parser"
%output="parser.tab.cpp"
%error-verbose
%debug
%start start

// The expected parser conflicts must be described beneath.
// One line for each type of conflict, in this form:
//
// (type)(number) cause of the conflict(s)
//
// (type) can be one of (s/r) or (r/r) (s = shift, r = reduce)
// (number) is the number of conflicts with the same cause
//
// (r/r)(1) reference_with_spec used for types as well as expressions
//
%expect 0
%expect-rr 1

// Initialize the initial location
//
%initial-action {
	@$.begin.filename = @$.end.filename = &filename;
	@$.begin.line     = @$.end.line     = 1;
	@$.begin.column   = @$.end.column   = 1;
};

////////////////////////////////////////////////////////////////////////////////
// Types of the Terminal and Non-terminal Symbols                             //
////////////////////////////////////////////////////////////////////////////////

%union {
	uint                                    t_small_int;
	BigInt*                                 t_int;
	bool                                    t_bool;
	string*                                 t_string;
	sptr<Declarations>*                     t_declarations;
	sptr<Declaration>*                      t_declaration;
	Detail::FunctionSignature*              t_function_signature;
	Detail::FunctionSections*               t_function_sections;
	sptr<FunctionDeclaration>*              t_function_declaration;
	sptr<TypeDeclaration>*                  t_type_declaration;
	vector<FunctionDeclaration::Parameter>* t_formal_parameter_list;
	FunctionDeclaration::Parameter*         t_formal_parameter;
	vector<VariableDeclaration::Pair>*      t_variable_declaration_list;
	VariableDeclaration::Pair*              t_variable_declaration_pair;
	sptr<VariableDeclaration>*              t_variable_declaration;
	sptr<Type>*                             t_type;
	sptr<FunctionType>*                     t_function_type;
	vector<sptr<Statement> >*               t_statement_list;
	Detail::Expression*                     t_expression;
	sptr<CompositeOperator>*                t_composite_operator;
	sptr<Statement>*                        t_statement;
	sptr<WhileStatement>*                   t_while_statement;
	sptr<AssertionArea>*                    t_assertion_area;
	set<sptr<Expression> >*                 t_expression_set; 
	vector<sptr<Expression> >*              t_expression_list;
	sptr<Reference>*                        t_reference;
	vector<sptr<Type> >*                    t_type_list;
	sptr<Identifier>*                       t_identifier;
	vector<sptr<Identifier> >*              t_identifier_list;
};

////////////////////////////////////////////////////////////////////////////////
// Rule Types                                                                 //
////////////////////////////////////////////////////////////////////////////////

%type <t_declarations>              declarations
%type <t_declaration>               declaration
%type <t_function_signature>        function_signature
%type <t_function_sections>         function_sections
%type <t_function_declaration>      function_declaration
%type <t_type_declaration>          type_declaration
%type <t_formal_parameter_list>     formal_parameter_list
                                    optional_formal_parameter_list
%type <t_formal_parameter>          formal_parameter
%type <t_variable_declaration_list> variable_declaration_list
%type <t_variable_declaration_pair> variable_declaration_pair
%type <t_variable_declaration>      variable_declaration
%type <t_type>                      type
%type <t_function_type>             function_type
%type <t_statement_list>            statement_sequence
                                    optional_statement_sequence
%type <t_statement>                 statement
%type <t_while_statement>           while_statement
                                    while_statement_sections
%type <t_expression>                expression
%type <t_assertion_area>            assertion_area
%type <t_expression_set>            expression_set
                                    optional_expression_set
%type <t_expression_list>           expression_list
                                    optional_expression_list
%type <t_string>                    reference_name
%type <t_reference>                 reference_no_spec
                                    reference_with_spec
%type <t_type_list>                 type_list
                                    optional_type_list
                                    formal_type_spec
                                    template_type_spec
%type <t_identifier>                identifier
%type <t_identifier_list>           identifier_list
                                    optional_identifier_list
                                    template_type_declaration

////////////////////////////////////////////////////////////////////////////////
// Giving String-literals to Some Terminal Symbols                            //
////////////////////////////////////////////////////////////////////////////////

%token SWAP_OP     "<->"
%token ASSIGN_OP   "<-"
%token MOD_OP      "mod"
%token PRE         "pre"
%token POST        "post"
%token LOGICAL     "logical"
%token BODY        "body"
%token DO          "do"
%token INVARIANT   "invariant"
%token BOUND       "bound"
%token OLDBOUND    "oldbound"
%token VOID        "void"
%token IF          "if"
%token THEN        "then"
%token ELSE        "else"
%token WHILE       "while"
%token INTERVAL_OP ".."
%token NEW         "new"
%token CPP         "cpp"
%token KEY         "KeY"
%token TYPE        "type"
%token FORALL      "forall"
%token THEREIS     "thereis"
%token END       0 "end of file"

////////////////////////////////////////////////////////////////////////////////
// Entrypoints                                                                //
////////////////////////////////////////////////////////////////////////////////

%token ENTER_DECLARATION
%token ENTER_DECLARATIONS
%token ENTER_FUNCTIONTYPE
%token ENTER_STATEMENT
%token ENTER_EXPRESSION
%token ENTER_REFERENCE
%token ENTER_TYPE

////////////////////////////////////////////////////////////////////////////////
// Other Token Declarations                                                   //
////////////////////////////////////////////////////////////////////////////////

%token <t_string>             IDENTIFIER
%token <t_int>                NUMBER
%token <t_bool>               TRUTH_VALUE
%token <t_string>             STRING_LITERAL
%token <t_composite_operator> RELATION_OP
%token <t_composite_operator> IMPLICATION_OP
%token <t_composite_operator> AND_OP
%token <t_composite_operator> OR_OP
%token <t_small_int>          PLACEHOLDER
%token                        ASSERTION_BEGIN
%token                        ASSERTION_END

////////////////////////////////////////////////////////////////////////////////
// Precedence Declarations                                                    //
////////////////////////////////////////////////////////////////////////////////

// An else-clause belongs to the deepest if-statement
//
%nonassoc IF_THEN_RULE
%nonassoc "else"

// Every do/invariant/bound clause belongs to the deepest loop statement.
//
%nonassoc WHILE_RULE
%nonassoc FUNCTION_DECLARATION_RULE
%nonassoc "do"
%nonassoc "bound"
%nonassoc "invariant"

// Operator Precedence
//
%nonassoc "<->"
%right    "<-"
%left     IMPLICATION_OP
%left     AND_OP
%left     OR_OP
%left     RELATION_OP
%left     ".."
%left     '+' '-'
%left     '*' '/' "mod"
%right    '!' '#' UNARY_PREFIX_OP
%left     '(' '['
%left     '.'

////////////////////////////////////////////////////////////////////////////////
// Top parser.tab.cpp code                                                    //
////////////////////////////////////////////////////////////////////////////////

%{
	#include "lexer.lex.hpp"
	
	#include <boost/assign.hpp>
	using namespace boost::assign;
	
	/// Report an error to the provided Messages class.
	///
	/// \pre messages != null
	///
	void yy::Parser::error(yy::location const& loc, string const& message) {
		assert(messages);
		messages->add(the(MessageInfo).extra("syntax-error", Error, message), loc);
	}
	
	/// Copy the value that \a v points to, return that value and deallocate \a v.
	///
	template <class T>
	T use(T* v) {
		T result = *v;
		delete v;
		return result;
	}
	
	/// Return a Detail::Expression struct of a unary operation on \a a.
	///
	/// \pre op is a unary operator
	///
	Detail::Expression* operator_call(sptr<Operator> op, Detail::Expression a) {
		sptr<OperatorCall> call = OperatorCall::construct(op);
		call->operands.push_back(a.expr);
		return new Detail::Expression(call);
	}
	
	/// Return a Detail::Expression struct of a binary operation on \a a and \a b.
	///
	/// \pre \a op is a non chain-associative binary operator
	///
	Detail::Expression* operator_call(sptr<Operator> op, Detail::Expression a, Detail::Expression b) {
		sptr<OperatorCall> call = OperatorCall::construct(op);
		call->operands.push_back(a.expr);
		call->operands.push_back(b.expr);
		return new Detail::Expression(call);
	}
	
	/// Return a Detail::Expression struct of a ternary operation on \a a, \a b and \a c.
	///
	/// \pre \a op is a ternary operator
	///
	Detail::Expression* operator_call(sptr<Operator> op, Detail::Expression a, Detail::Expression b, Detail::Expression c) {
		sptr<OperatorCall> call = OperatorCall::construct(op);
		call->operands.push_back(a.expr);
		call->operands.push_back(b.expr);
		call->operands.push_back(c.expr);
		return new Detail::Expression(call);
	}
	
	/// Return a Detail::Expression struct of a binary operation on \a a and \a b.
	/// Automatically links \a b to \a a, if \a a is already a chain. Otherwise,
	/// starts a new chain.
	///
	/// \pre \a op is a binary chain-associative operator of chain-type \a type
	///
	Detail::Expression* operator_chain(sptr<Operator> op, Detail::Expression a, Detail::Expression b, Detail::ChainType type) {
		sptr<ChainExpression> result;
		if (a.chain == type) {
			result = a.expr.cast<ChainExpression>();
		} else {
			result = ChainExpression::construct();
			result->operands.push_back(a.expr);
		}
		result->operators.push_back(op);
		result->operands.push_back(b.expr);
		return new Detail::Expression(result, type);
	}
	
%}

%%

/******************************************************************************
 * Grammar                                                                    *
 ******************************************************************************/

start:
	ENTER_DECLARATION declaration {
		output = use($2);
	} |
	ENTER_DECLARATIONS declarations {
		output = use($2);
	} |
	ENTER_FUNCTIONTYPE function_type {
		output = use($2);
	} |
	ENTER_STATEMENT statement {
		output = use($2);
	} |
	ENTER_EXPRESSION expression {
		output = use($2).expr;
	} |
	ENTER_REFERENCE reference_with_spec {
		output = use($2);
	} |
	ENTER_TYPE type {
		output = use($2);
	}
;

// sptr<Declarations>*
//
declarations:
	declarations declaration {
		$$ = $1;
		(*$$)->declarations.push_back(use($2));
		(*$$)->location = @$;
	} |
	declarations error {
		$$ = $1;
		(*$$)->location = @$;
	} |
	declarations error ';' {
		$$ = $1;
		(*$$)->location = @$;
	} |
	/*empty*/ {
		$$ = n_sptr_ptr(Declarations::construct());
	}
;

// sptr<Declaration>*
//
declaration:
	function_declaration {
		$$ = new sptr<Declaration>(use($1));
		(*$$)->location = @$;
	} |
	variable_declaration {
		$$ = new sptr<Declaration>(use($1));
		(*$$)->location = @$;
	} |
	type_declaration {
		$$ = new sptr<Declaration>(use($1));
		(*$$)->location = @$;
	}
;

// sptr<VariableDeclaration>*
//
variable_declaration:
	type variable_declaration_list ';' {
		$$ = n_sptr_ptr(VariableDeclaration::construct(use($1), use($2)));
		(*$$)->type->parent = *$$;
		(*$$)->location = @$;
	}
;

// vector<sptr<Identifier> >*
//
template_type_declaration:
	'?' '(' optional_identifier_list ')' {
		$$ = $3;
	}
;

// vector<sptr<Identifier> >*
//
identifier_list:
	identifier_list ',' identifier {
		$$ = $1;
		$$->push_back(use($3));
	} |
	identifier {
		$$ = new vector<sptr<Identifier> >;
		$$->push_back(use($1));
	}
;

// vector<sptr<Identifier> >*
//
optional_identifier_list:
	identifier_list |
	/* empty */ {
		$$ = new vector<sptr<Identifier> >;
	}
;

// sptr<TypeDeclaration>*
//
type_declaration:
	"type" identifier "cpp" STRING_LITERAL "KeY" STRING_LITERAL ';' {
		$$ = n_sptr_ptr(TypeDeclaration::construct(use($2), use($4), use($6)));
		(*$$)->location = @$;
	}
;

// sptr<FunctionDeclaration>*
//
function_declaration:
	function_signature function_sections %prec FUNCTION_DECLARATION_RULE {
		$$ = n_sptr_ptr(FunctionDeclaration::construct());
		(*$$)->type              = $1->type;
		(*$$)->name              = $1->name;
		(*$$)->parameterNames    = $1->parameterNames;
		(*$$)->templateTypeNames = $1->templateTypeNames;
		(*$$)->isTemplateInstantiation = false;
		delete $1;
		(*$$)->logicalVars = $2->logicalVars;
		(*$$)->pre         = $2->pre;
		(*$$)->post        = $2->post;
		(*$$)->bound       = $2->bound;
		(*$$)->KeY         = $2->KeY;
		(*$$)->body        = $2->body;
		delete $2;
		(*$$)->location = @$;
	}
;

// Detail::FunctionSignature*
//
function_signature:
	type identifier '(' optional_formal_parameter_list ')' {
		$$ = new Detail::FunctionSignature;
		$$->type = FunctionType::construct(use($1));
		$$->name = use($2);
		foreach (FunctionDeclaration::Parameter param, use($4)) {
			$$->type->parameterTypes.push_back(param.type);
			$$->parameterNames.push_back(param.name);
		}
	} |
	type identifier template_type_declaration '(' optional_formal_parameter_list ')' {
		$$ = new Detail::FunctionSignature;
		$$->type = FunctionType::construct(use($1));
		$$->name = use($2);
		foreach (FunctionDeclaration::Parameter param, use($5)) {
			$$->type->parameterTypes.push_back(param.type);
			$$->parameterNames.push_back(param.name);
		}
		$$->templateTypeNames = use($3);
	}
;

// Detail::FunctionSections*
//
function_sections:
	'{' optional_statement_sequence '}' {
		$$ = new Detail::FunctionSections;
		(*$$->body.insert(CompoundStatement::construct(use($2))).first)->location = @$;
	} |
	"body" '{' optional_statement_sequence '}' {
		$$ = new Detail::FunctionSections;
		(*$$->body.insert(CompoundStatement::construct(use($3))).first)->location = @$;
	} |
	"pre" '{' assertion_area '}' {
		$$ = new Detail::FunctionSections;
		(*$$->pre.insert(use($3)).first)->location = @$;
	} |
	"post" '{' assertion_area '}' {
		$$ = new Detail::FunctionSections;
		(*$$->post.insert(use($3)).first)->location = @$;
	} |
	"bound" '(' expression ')' {
		$$ = new Detail::FunctionSections;
		(*$$->bound.insert(use($3).expr).first)->location = @$;
	} |
	"KeY" STRING_LITERAL {
		$$ = new Detail::FunctionSections;
		$$->KeY.insert(use($2));
	} |
	"logical" variable_declaration {
		$$ = new Detail::FunctionSections;
		(*$$->logicalVars.insert(use($2)).first)->location = @$;
	} |
	function_sections "body" '{' optional_statement_sequence '}' {
		$$ = $1;
		(*$$->body.insert(CompoundStatement::construct(use($4))).first)->location = Location(@2, @5);
	} |
	function_sections "pre" '{' assertion_area '}' {
		$$ = $1;
		(*$$->pre.insert(use($4)).first)->location = Location(@2, @5);
	} |
	function_sections "post" '{' assertion_area '}' {
		$$ = $1;
		(*$$->post.insert(use($4)).first)->location = Location(@2, @5);
	} |
	function_sections "bound" '(' expression ')' {
		$$ = $1;
		(*$$->bound.insert(use($4).expr).first)->location = @$;
	} |
	function_sections "KeY" STRING_LITERAL {
		$$ = $1;
		$$->KeY.insert(use($3));
	} |
	function_sections "logical" variable_declaration {
		$$ = $1;
		$$->logicalVars.insert(use($3));
	}
;

// vector<FunctionDeclaration::Parameter>*
//
formal_parameter_list:
	formal_parameter_list ',' formal_parameter {
		$$ = $1;
		$$->push_back(use($3));
	} |
	formal_parameter {
		$$ = new vector<FunctionDeclaration::Parameter>;
		$$->push_back(use($1));
	}
;

// vector<FunctionDeclaration::Parameter>*
//
optional_formal_parameter_list:
	formal_parameter_list |
	/* empty */ {
		$$ = new vector<FunctionDeclaration::Parameter>;
	}
;

// FunctionDeclaration::Parameter*
//
formal_parameter:
	type identifier {
		$$ = new FunctionDeclaration::Parameter(use($1), use($2));
	}
;

// vector<VariableDeclaration::Pair>*
//
variable_declaration_list:
	variable_declaration_list ',' variable_declaration_pair {
		$$ = $1;
		$$->push_back(use($3));
	} |
	variable_declaration_pair {
		$$ = new vector<VariableDeclaration::Pair>;
		$$->push_back(use($1));
	}
;

// VariableDeclaration::Pair*
//
variable_declaration_pair:
	identifier {
		$$ = new VariableDeclaration::Pair(use($1));
	} |
	identifier "<-" expression {
		$$ = new VariableDeclaration::Pair(use($1), use($3).expr);
	} |
	identifier "<-" error {
		$$ = new VariableDeclaration::Pair(use($1));
	}
;

// sptr<Type>*
//
type:
	"void" {
		$$ = new sptr<Type>(VoidType::construct());
		(*$$)->location = @$;
	} |
	reference_with_spec {
		$$ = new sptr<Type>(NamedType::construct(use($1)));
		(*$$)->location = @$;
	} |
	type '[' ']' {
		$$ = new sptr<Type>(ArrayType::construct(use($1)));
		(*$$)->location = @$;
	}
;

// sptr<FunctionType>*
//
function_type:
	type '(' optional_type_list ')' {
		$$ = n_sptr_ptr(FunctionType::construct(use($1), use($3)));
		(*$$)->location = @$;
	}
;

// vector<sptr<Statement> >*
//
statement_sequence:
	statement_sequence statement {
		$$ = $1;
		$$->push_back(use($2));
	} |
	statement {
		$$ = new vector<sptr<Statement> >;
		$$->push_back(use($1));
	}
;

// vector<sptr<Statement> >*
//
optional_statement_sequence:
	statement_sequence |
	/* empty */ {
		$$ = new vector<sptr<Statement> >;
	}
;

// Detail::Expression*
//
expression:
	expression "<->" expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 <-> 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression "<-" expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 <- 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression OR_OP expression {
		$$ = operator_call(use($2), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression AND_OP expression {
		$$ = operator_call(use($2), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression IMPLICATION_OP expression {
		$$ = operator_chain(use($2), use($1), use($3), Detail::IMPLIES_CHAIN);
		$$->expr->location = @$;
	} |
	expression RELATION_OP expression {
		$$ = operator_chain(use($2), use($1), use($3), Detail::COMPARISON_CHAIN);
		$$->expr->location = @$;
	} |
	expression ".." expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 .. 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression '+' expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 + 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression '-' expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 - 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression '*' expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 * 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression '/' expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 / 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	expression "mod" expression {
		$$ = operator_call(n_sptr(new SingleOperator("1 mod 2")), use($1), use($3));
		$$->expr->location = @$;
	} |
	'!' expression {
		$$ = operator_call(n_sptr(new SingleOperator("! 1")), use($2));
		$$->expr->location = @$;
	} |
	'#' expression {
		$$ = operator_call(n_sptr(new SingleOperator("# 1")), use($2));
		$$->expr->location = @$;
	} |
	'-' expression %prec UNARY_PREFIX_OP {
		$$ = operator_call(n_sptr(new SingleOperator("- 1")), use($2));
		$$->expr->location = @$;
	} |
	'+' expression %prec UNARY_PREFIX_OP {
		$$ = operator_call(n_sptr(new SingleOperator("+ 1")), use($2));
		$$->expr->location = @$;
	} |
	expression '(' optional_expression_list ')' {
		$$ = new Detail::Expression(FunctionCall::construct(use($1).expr, use($3)));
		$$->expr->location = @$;
	} |
	expression '[' expression ']' {
		$$ = operator_call(n_sptr(new SingleOperator("1 [ 2 ]")), use($1), use($3));
		$$->expr->location = @$;
	} |
	"if" '(' expression ')' "then" expression "else" expression {
		$$ = operator_call(n_sptr(new SingleOperator("if ( 1 ) then 2 else 3")), use($3), use($6), use($8));
		$$->expr->location = @$;
	} |
	"forall" '(' identifier ':' expression ".." expression ')' '(' expression ')' {
		$$ = new Detail::Expression(ForallExpression::construct(use($3), use($5).expr, use($7).expr, use($10).expr));
		$$->expr->location = @$;
	} |
	"thereis" '(' identifier ':' expression ".." expression ')' '(' expression ')' {
		$$ = new Detail::Expression(ThereisExpression::construct(use($3), use($5).expr, use($7).expr, use($10).expr));
		$$->expr->location = @$;
	} |
	reference_with_spec {
		$$ = new Detail::Expression(use($1));
		$$->expr->location = @$;
	} |
	TRUTH_VALUE {
		$$ = new Detail::Expression(BooleanLiteral::construct($1));
		$$->expr->location = @$;
	} |
	NUMBER {
		$$ = new Detail::Expression(IntegerLiteral::construct(use($1)));
		$$->expr->location = @$;
	} |
	'(' expression ')' {
		$$ = $2;
		$$->chain = Detail::NO_CHAIN;
		$$->expr->location = @$;
	} |
	PLACEHOLDER {
		if (insertions.size() < $1 || !(insertions.at($1 - 1))) {
			messages->add("unexpected", @1, "placeholder");
			YYERROR;
		}
		$$ = new Detail::Expression(insertions.at($1 - 1));
		insertions.at($1 - 1) = sptr<Expression>();
	}
;

// sptr<Statement>*
//
statement:
	declaration {
		$$ = new sptr<Statement>(use($1));
		(*$$)->location = @$;
	} |
	expression ';' {
		$$ = new sptr<Statement>(use($1).expr);
		(*$$)->location = @$;
	} |
	"if" '(' expression ')' "then" statement %prec IF_THEN_RULE {
		sptr<CompoundStatement> thenStatement;
		if (typeid(**$6) == typeid(CompoundStatement))
			thenStatement = use($6).cast<CompoundStatement>();
		else
			thenStatement = CompoundStatement::construct(list_of(use($6)));
		$$ = new sptr<Statement>(IfStatement::construct(use($3).expr, thenStatement));
		(*$$)->location = @$;
	} |
	"if" '(' expression ')' "then" statement "else" statement {
		sptr<CompoundStatement> thenStatement;
		if (typeid(**$6) == typeid(CompoundStatement))
			thenStatement = use($6).cast<CompoundStatement>();
		else
			thenStatement = CompoundStatement::construct(list_of(use($6)));
		sptr<CompoundStatement> elseStatement;
		if (typeid(**$8) == typeid(CompoundStatement))
			elseStatement = use($8).cast<CompoundStatement>();
		else
			elseStatement = CompoundStatement::construct(list_of(use($8)));
		$$ = new sptr<Statement>(IfStatement::construct(use($3).expr, thenStatement, elseStatement));
		(*$$)->location = @$;
	} |
	while_statement {
		$$ = new sptr<Statement>(use($1));
		(*$$)->location = @$;
	} |
	'{' optional_statement_sequence '}' {
		$$ = new sptr<Statement>(CompoundStatement::construct(use($2)));
		(*$$)->location = @$;
	} |
	identifier '{' optional_statement_sequence '}' {
		$$ = new sptr<Statement>(CompoundStatement::construct(use($1), use($3)));
		(*$$)->location = @$;
	} |
	assertion_area {
		$$ = new sptr<Statement>(use($1));
		(*$$)->location = @$;
	} |
	"cpp" STRING_LITERAL ';' {
		$$ = new sptr<Statement>(CppStatement::construct(use($2)));
	}
;

// sptr<WhileStatement>*
//
while_statement:
	"while" '(' expression ')' while_statement_sections %prec WHILE_RULE {
		$$ = $5;
		(*$$)->condition = use($3).expr;
		(*$$)->location = @$;
	}
;

// sptr<WhileStatement>*
//
while_statement_sections:
	statement {
		sptr<CompoundStatement> statement;
		if (typeid(**$1) == typeid(CompoundStatement))
			statement = use($1).cast<CompoundStatement>();
		else
			statement = CompoundStatement::construct(list_of(use($1)));
		$$ = n_sptr_ptr(WhileStatement::construct());
		(*$$)->statement.insert(statement);
	} |
	"do" statement {
		sptr<CompoundStatement> statement;
		if (typeid(**$2) == typeid(CompoundStatement))
			statement = use($2).cast<CompoundStatement>();
		else
			statement = CompoundStatement::construct(list_of(use($2)));
		$$ = n_sptr_ptr(WhileStatement::construct());
		(*$$)->statement.insert(statement);
	} |
	"bound" '(' expression ')' {
		$$ = n_sptr_ptr(WhileStatement::construct());
		(*$$)->bound.insert(use($3).expr);
	} |
	"invariant" '{' assertion_area '}' {
		$$ = n_sptr_ptr(WhileStatement::construct());
		(*$$)->invariant.insert(use($3));
	} |
	while_statement_sections "do" statement {
		$$ = $1;
		sptr<CompoundStatement> statement;
		if (typeid(**$3) == typeid(CompoundStatement))
			statement = use($3).cast<CompoundStatement>();
		else
			statement = CompoundStatement::construct(list_of(use($3)));
		(*$$)->statement.insert(statement);
	} |
	while_statement_sections "bound" '(' expression ')' {
		$$ = $1;
		(*$$)->bound.insert(use($4).expr);
	} |
	while_statement_sections "invariant" '{' assertion_area '}' {
		$$ = $1;
		(*$$)->invariant.insert(use($4));
	}
;

// sptr<AssertionArea>*
//
assertion_area:
	ASSERTION_BEGIN optional_expression_set ASSERTION_END {
		$$ = n_sptr_ptr(AssertionArea::construct(use($2)));
		(*$$)->location = Location(@1, @2);
	}
;

// set<sptr<Expression> >*
//
expression_set:
	expression_set expression ';' {
		$$ = $1;
		$$->insert(use($2).expr);
	} |
	expression ';' {
		$$ = new set<sptr<Expression> >;
		$$->insert(use($1).expr);
	}
;

// set<sptr<Expression> >*
//
optional_expression_set:
	expression_set |
	/* empty */ {
		$$ = new set<sptr<Expression> >;
	}
;

// vector<sptr<Expression> >*
//
expression_list:
	expression_list ',' expression {
		$$ = $1;
		$$->push_back(use($3).expr);
	} |
	expression {
		$$ = new vector<sptr<Expression> >;
		$$->push_back(use($1).expr);
	}
;

// vector<sptr<Expression> >*
//
optional_expression_list:
	expression_list |
	/* empty */ {
		$$ = new vector<sptr<Expression> >;
	}
;

// string*
//
reference_name:
	IDENTIFIER |
	"oldbound" {
		$$ = new string("oldbound");
	}
;

// sptr<Reference>*
//
reference_no_spec:
	reference_with_spec '.' reference_name {
		$$ = n_sptr_ptr(Reference::construct(use($1), use($3)));
	} |
	'.' reference_name {
		$$ = n_sptr_ptr(Reference::construct(Reference::construct(), use($2)));
	} |
	reference_name {
		$$ = n_sptr_ptr(Reference::construct(use($1)));
	}
;

// sptr<Reference>*
//
reference_with_spec:
	reference_no_spec {
		$$ = $1;
		(*$$)->location = @$;
	} |
	reference_no_spec formal_type_spec  {
		$$ = $1;
		(*$$)->formalTypeSpec = use($2);
		(*$$)->location = @$;
	} |
	reference_no_spec formal_type_spec template_type_spec {
		$$ = $1;
		(*$$)->formalTypeSpec   = use($2);
		(*$$)->templateTypeSpec = use($3);
		(*$$)->location = @$;
	} |
	reference_no_spec template_type_spec {
		$$ = $1;
		(*$$)->templateTypeSpec = use($2);
		(*$$)->location = @$;
	} |
	reference_no_spec template_type_spec formal_type_spec {
		$$ = $1;
		(*$$)->templateTypeSpec = use($2);
		(*$$)->formalTypeSpec   = use($3);
		(*$$)->location = @$;
	}
;

// vector<sptr<Type> >*
//
formal_type_spec:
	'!' '(' optional_type_list ')' {
		$$ = new vector<sptr<Type> >(use($3));
	}
;

// vector<sptr<Type> >*
//
template_type_spec:
	'?' '(' optional_type_list ')' {
		$$ = new vector<sptr<Type> >(use($3));
	}
;

// vector<sptr<Type> >*
//
optional_type_list:
	type_list |
	/* empty */ {
		$$ = new vector<sptr<Type> >;
	}
;

// vector<sptr<Type> >*
//
type_list:
	type_list ',' type {
		$$ = $1;
		$$->push_back(use($3));
	} |
	type {
		$$ = new vector<sptr<Type> >;
		$$->push_back(use($1));
	}
;

// sptr<Identifier>*
//
identifier:
	IDENTIFIER {
		$$ = n_sptr_ptr(Identifier::construct(use($1)));
		(*$$)->location = @$;
	}
;
